Nuprl Lemma : isect2_decomp
4,23
postcript
pdf
t1
,
t2
:Type,
x
:
t1
t2
.
x
t1
&
x
t2
latex
Definitions
P
&
Q
,
T1
T2
,
x
:
A
.
B
(
x
)
,
t
T
,
true
,
false
Lemmas
bfalse
wf
,
member
wf
,
btrue
wf
,
isect2
wf
origin
t1, t2:Type, x:t1 
t2. x 
t1 & x t2 t1, t2:Type, x:t1 t2. x t1 & x t2 T2x:A. B(x) T